i, j:. (i = j)  ((i = j) ~ tt) 

latex

Up	sqequal 1, sqequal 1
Definitions	, t  T, P  Q, x:A. B(x), {T}, SQType(T), P & Q, P  Q, P  Q
Lemmas	bool sq, assert of eq int, eqtt to assert, assert wf, btrue wf, eq int wf, bool wf, iff transitivity